We provide a simple translation of the satisfiability problem for regular grammar logics with converse into GF2, which is the intersection of the guarded fragment and the 2-variable fragment of first-order logic. The translation is theoretically interesting because it translates modal logics with certain frame conditions into first-order logic, without explicitly expressing the frame conditions. It is practically relevant because it makes it possible to use a decision procedure for the guarded fragment in order to decide regular grammar logics with (...) converse. The class of regular grammar logics includes numerous logics from various application domains. A consequence of the translation is that the general satisfiability problem for every regular grammar logics with converse is in EXPTIME. This extends a previous result of the first author for grammar logics without converse. Other logics that can be translated into GF2 include nominal tense logics and intuitionistic logic. In our view, the results in this paper show that the natural first-order fragment corresponding to regular grammar logics is simply GF2 without extra machinery such as fixed-point operators. (shrink)

We show that the E + -class can be decided by resolution using a liftable order, when the order is applied a posteriori. This is a surprising result, because the decision procedure for the E + -class was one of the motivations for the study of non-liftable orders. Also surprising is the behaviour of the resolution process. Initially the maximal depth at which a variable occurs can increase, but it will not increase more than a certain bound. We do not (...) make use of any type of saturation rule in our resolution strategy. (shrink)